st-key-match(tab;k1;k2)
== Case k1 of
== inl(n)  Case k2 of inl(m)  false ; inr(a)  n<ptr(tab)  n<||tab||   st-atom(tab;n) =a1 a
== inr(a)  Case k2 of
== inr(a)  inl(n)  n<ptr(tab)  n<||tab||   st-atom(tab;n) =a1 a
== inr(a)  inr(b)  false 

latex

---

clarification:

st-key-match(tab;k1;k2)
== Case k1 of
== inl(n)  Case k2 of
== inl(n)  inl(m)  false
== inl(n)  inr(a)  n<ptr(tab)  n<||tab||   eq_atom1(st-atom(tab;n);a)
== inr(a)  Case k2 of
== inr(a)  inl(n)  n<ptr(tab)  n<||tab||   eq_atom1(st-atom(tab;n);a)
== inr(a)  inr(b)  false 

latex

Definitions	Case b of inl(x)  s(x) ; inr(y)  t(y), p  q, ptr(tab), i<j, ||tab|| , eq_atom$n(x;y), st-atom(tab;n), false
FDL editor aliases	st-key-match